T:Type, P:(T), L:(T List) List. filter(P;concat(L)) ~ concat(map(l.filter(P;l);L)) 

latex

Definitions	map(f;as), filter(P;l), S  T, Top, as @ bs, concat(ll), , x:A. B(x), t  T
Lemmas	bool wf, top wf, concat-cons, filter append sq